package com.googlecode.kipler.satisfiability.reasoner;

import java.util.HashSet;
import java.util.LinkedHashSet;
import java.util.Set;

import com.googlecode.kipler.container.dl.BasicWcsInterpolationData;
import com.googlecode.kipler.container.dl.LabelManager;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.container.dl.operational.IndividualNameManager;
import com.googlecode.kipler.satisfiability.completion.branching.AbstractBacktracking;
import com.googlecode.kipler.satisfiability.completion.branching.BacktrackingAlgorithm;
import com.googlecode.kipler.satisfiability.completion.branching.BacktrackingAlgorithmFactory;
import com.googlecode.kipler.satisfiability.completion.branching.BranchingPoint;
import com.googlecode.kipler.satisfiability.completion.branching.LinearBranchingPoint;
import com.googlecode.kipler.satisfiability.completion.rule.RuleLogger;
import com.googlecode.kipler.satisfiability.completion.strategy.CompletionStrategy;
import com.googlecode.kipler.satisfiability.reasoner.profile.ReasoningProfile;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.Formula;

/**
 * This is the default implementation of the {@link Reasoner} interface.
 * 
 * @author İnanç Seylan
 * 
 */
public class GenericReasoner implements SATReasoner, InterpolantReasoner {

	private WorldConstraintSystem currentWcs;

	private BranchingPoint currentPoint;

	private int lastWcsId;

	private ReasoningProfile profile;

	private Set<Formula> formulaSet = new LinkedHashSet<Formula>();

	private AbstractBacktracking backtrackingAlg;

	public GenericReasoner() {
	}

	public ReasoningProfile getProfile() {
		return profile;
	}

	public void setProfile(ReasoningProfile profile) {
		this.profile = profile;
	}

	/**
	 * This method should only be called after {@link #isSatisfiable()} or
	 * {@link #isLogicalConsequence(Formula)}.
	 * 
	 * @return the last {@link WorldConstraintSystem} that the reasoner had
	 *         modified when the tableau algorithm ended.
	 */
	public WorldConstraintSystem getCurrentWcs() {
		return currentWcs;
	}

	/**
	 * @see Reasoner#addFormula(Formula)
	 */
	public void addFormula(Formula formula) {
		formulaSet.add(formula);
	}

	/**
	 * @see Reasoner#addFormulas(Set)
	 */
	public void addFormulas(Set<Formula> formulas) {
		formulaSet.addAll(formulas);
	}

	/**
	 * Applies the rules of tableau to all worlds in a world constraint system.
	 * The case of the disjunction rule is treated specially. If the disjunction
	 * rule is applied to a wcs, this method ends for that wcs.
	 * 
	 */
	private void applyRules() throws ReasonerException {
		CompletionStrategy cs = getProfile().getCompletionStrategy();
		if (cs != null) {
			cs.apply(getCurrentWcs());
		}
	}

	/**
	 * Adds the branching point to the stack.
	 */
	public void addBranch(BranchingPoint bp) {
		currentPoint.setNextBranchingPoint(bp);
		// the application of rules should continue from the next branching
		// point
		currentPoint = bp;
	}

	private WorldConstraintSystem preprocess(Set<Formula> formulaSet) {
		return getProfile().getPreprocessingStrategy().process(formulaSet);
	}

	/**
	 * @see Reasoner#isSatisfiable()
	 */
	public boolean isSatisfiable() throws Exception {
		return isSatisfiable(formulaSet);
	}

	/**
	 * This method actually applies the satisfiability checking algorithm on the
	 * knowledge base plus the negation of the input formula.
	 * 
	 * @return true if the knowledge base plus the negation of the input formula
	 *         is unsatisfiable.
	 * @see Reasoner#isLogicalConsequence(Formula)
	 */
	public boolean isLogicalConsequence(Formula formula) throws Exception {
		Formula negFormula = formula.copy().toggleNegated();
		Set<Formula> formulaSetCopy = new LinkedHashSet<Formula>(formulaSet);
		formulaSetCopy.add(negFormula);
		return !isSatisfiable(formulaSetCopy);
	}

	public boolean isLogicalConsequence(Set<Formula> formulaSet, Formula formula)
			throws Exception {
		Formula negFormula = formula.copy().toggleNegated();
		Set<Formula> formulaSetCopy = new LinkedHashSet<Formula>(formulaSet);
		formulaSetCopy.add(negFormula);
		return !isSatisfiable(formulaSetCopy);
	}

	private void initProver(Set<Formula> formulaSet) {
		currentWcs = preprocess(formulaSet);
		lastWcsId = 0;
		IndividualNameManager.getInstance().reset();
		currentWcs.setId(lastWcsId);
		currentWcs.getData().getLogger().setEnabled(
				getProfile().isLoggingEnabled());
		backtrackingAlg = getProfile().isBackjumpingEnabled() ? BacktrackingAlgorithmFactory
				.createAlgorithm(BacktrackingAlgorithm.BACKJUMPING)
				: BacktrackingAlgorithmFactory
						.createAlgorithm(BacktrackingAlgorithm.BACKTRACKING);
	}

	private boolean isSatisfiable(Set<Formula> formulaSet) {
		initProver(formulaSet);
		return sat();
	}

	private boolean sat() {
		// if the initial world constraint system is unsatisfiable already
		if (!currentWcs.getWorld("w0").isSatisfiable()) {
			return false;
		}
		boolean satisfiable = false;
		currentPoint = new LinearBranchingPoint(currentWcs);
		do {
			try {
				currentWcs = currentPoint.nextBranch();
				applyRules();
				satisfiable = true;
			} catch (BranchingException e) {
				satisfiable = false;
			} catch (UnsatisfiableException e) {
				satisfiable = false;
				getLogger().info(
						"WCS " + getCurrentWcs().getId()
								+ " is unsatisfiable. Cause "
								+ e.getExplanation());
				backtrackingAlg.setCurrentPoint(currentPoint);
				backtrackingAlg.setException(e);
				currentPoint = backtrackingAlg.apply();
			} catch (ReasonerException e) {
				// will never come here
			}
		} while (currentPoint.isBranchingPossible() && !satisfiable);
		currentWcs = currentPoint.getWcs();
		return satisfiable;
	}

	private RuleLogger getLogger() {
		return currentWcs.getData().getLogger();
	}

	@Override
	public Concept interpolant(Set<Formula> leftTheory,
			Set<Formula> rightTheory, Concept leftConcept, Concept rightConcept)
			throws Exception {
		// TODO syntactic check that formulas do not contain named individuals
		if (!getProfile().isInterpolationEnabled()) {
			getProfile().toggleInterpolation();
		}
		Set<Formula> wholeTheory = new HashSet<Formula>(leftTheory);
		wholeTheory.addAll(rightTheory);
		initProver(wholeTheory);
		LabelManager labelMan = ((BasicWcsInterpolationData) currentWcs
				.getData()).getLabelManager();
		for (Formula f : leftTheory) {
			labelMan.setLabel(f, true);
		}
		for (Formula f : rightTheory) {
			labelMan.setLabel(f, false);
		}
		String indvName = IndividualNameManager.getInstance()
				.generateIndividualName();
		ConceptAssertion caLeft = new ConceptAssertion(leftConcept, indvName);
		ConceptAssertion caRight = new ConceptAssertion(rightConcept, indvName)
				.toggleNegated();
		labelMan.setLabel(caLeft, true);
		labelMan.setLabel(caRight, false);
		currentWcs.getWorld("w0").add(caLeft);
		currentWcs.getWorld("w0").add(caRight);
		if (!sat()) {
			return ((BasicWcsInterpolationData) currentWcs.getData())
					.getInterpolant().getConcept();
		}
		return null;
	}
}
